A:Type, eq:EqDecider(A), x,y:A, v:top.
sqequal(fpf-dom(eq; x; fpf-single(y; v)); (eqof(eq)(y,x))) 

latex

Definitions	x:A. B(x), fpf-dom(eq; x; f), fpf-single(x; v), deq-member(eq; x; L), t.1, reduce(f; k; as), bor(p; q), ff, Y, t  T, P  Q, tt, if b then t else f fi , prop{i:l}, , Unit, P  Q, P  Q,
Lemmas	eqof wf, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, top wf, deq wf